This PR adds `GetElem` lemmas for the basic `Vector` operations.

The `Vector` API is still very sparse, but I'm hoping to infill rapidly.

This PR removes unnecessary parameters from the funcion induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.

Part 1, before stage0 update.

Closes leanprover#6320

This PR removes unnecessary parameters from the funcion induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.

Part 2, adjusting after stage0 update.

Closes leanprover#6320

This PR adds missing `(types := true)` to `#reduce` example in [Readers
example](https://lean-lang.org/lean4/doc/monads/readers.lean.html).
Since [4.10](https://lean-lang.org/blog/2024-8-1-lean-4100/) the `(types
:= true)` is necessary for the `ReaderM Environment String` type to be
reduced into `Environment → String`.

…rover#6322)

This PR removes the deprecated aliases `Int.div := Int.tdiv` and
`Int.mod := Int.tmod`. Later we will rename `Int.ediv` to `Int.div` and
`Int.emod` to `Int.mod`.

This PRs continues cleaning up Array lemmas and improving alignment with
List.

This PR lets `_` be used in numeric literals as a separator. For
example, `1_000_000`, `0xff_ff` or `0b_10_11_01_00`. New lexical syntax:
```text
numeral10 : [0-9]+ ("_"+ [0-9]+)*
numeral2  : "0" [bB] ("_"* [0-1]+)+
numeral8  : "0" [oO] ("_"* [0-7]+)+
numeral16 : "0" [xX] ("_"* hex_char+)+
float     : numeral10 "." numeral10? [eE[+-]numeral10]
```

Closes leanprover#6199

Further alignment of `Array` and `List` lemmas. Moved lemmas about
`List.toArray` to a separate file, and aligned lemmas about membership.

Continuing cleanup of Array lemmas.